Morgan and Back have proposed different formalisations of procedures and parameters in the context of techniques of program development based on refinement. In this paper, we investigate a surprising and intricate relationship between these works and the substitution operator that renames the free variables of a program. In this study, we reveal an inconsistency in Morgan's refinement calculus and show that Back's formalisation of procedures does not have the same problem.
展开▼